00010	(DE TREE(L)
00020	(COND((ATOM(CDR (ANCESTOR L)))(LIST L))
00030	    (T(NCONC(LIST L)(TREE(CAR(ANCESTOR L)))(TREE(CDR(ANCESTOR L)))))) )
00040	
00100	(DE MATCHER(L TREE)
00200	(PROG NIL
00300	A(COND((NULL L)(RETURN NIL))
00400	  ((MEMQ (CAR L) TREE)(RETURN T)))
00500	(SETQ L(CDR L))(GO A)))
00600	
00700	(DF *CLM(L)(*CL(CAR L) CLAUSES))
00800	(DE OCNP(P C)
00900	(PROG (Z )
01000	(COND((ALLPOS C)(RETURN NIL)))
01100	(SETQ Z(NEGL C))
01200	(COND((ATOM P)(RETURN(OCNPL P Z))))
01210	(RETURN(OCNP1 P Z)) ))
01220	(DE OCNP1(P Z)(PROG(Z1)
01300	B(SETQ Z1(CDAR Z))
01400	(COND((NOT(EQ(CAR P)(CAR Z1)))NIL)
01500	     ((UNI(CDR P)(CDR Z1) NIL)(RETURN T)))
01600	(SETQ Z(CDR Z))
01700	(COND(Z(GO B)))(RETURN NIL)
01800	))
01900	
02000	(DE OCNPL(P C)
02100	(PROG NIL
02200	A(COND((EQ P(CADAR C))(RETURN T)))
02300	(SETQ C(CDR C))(COND (C(GO A)))(RETURN NIL) ))
02400	
02500	(DE OCPP(P C)
02600	(PROG (Z)
02700	(COND((ALLNEG C)(RETURN (OCNP P C))))
02800	(SETQ Z(NEGL C))
02900	(SETQ C(CDR C))
03000	(COND((ATOM P)(RETURN (OCPPL P C Z))))
03100	B(COND((NOT (EQ(CAR P)(CAAR C)))NIL)
03200	   ((UNI(CDR P)(CDAR C)NIL)(RETURN T)))
03300	(SETQ C(CDR C))
03400	(COND((NOT (EQ C Z))(GO B))((NULL C)(RETURN NIL)))
03450	
03500	(RETURN(OCNP1 P Z)) ))
03600	
03700	(DE OCPPL (P C Z)
03800	(PROG  NIL
03900	A(COND((EQ P(CAAR C))(RETURN T)))
04000	(SETQ C(CDR C))
04100	(COND((NOT (EQ C Z))(GO A))((NULL C)(RETURN NIL)))
04200	(RETURN (OCNPL P Z)) ))
     

00100	
00200	
00300	(DEFPROP VARIT1 
00400	 (LAMBDA(Z)
00500	  (PROG (Z1 Z2 Z3)
00600		(SETQ Z3 Z)
00700	   M1   (SETQ Z2 (CAR Z))
00800		(COND ((VAR Z2)
00900		       (COND ((SETQ Z1 (ASSOC Z2 BL)) (RPLACA Z (CDR Z1)))
01000			     (T (SETQ BL (CONS (CONS Z2 (SETQ NO (ADD1 NO))) BL)) (RPLACA Z NO))))
01100		      ((CONST Z2) NIL)
01200		      (T (VARIT1 (CDR Z2))))
01300		(SETQ Z (CDR Z))
01400		(COND (Z (GO M1)))
01500		(RETURN Z3))) 
01600	EXPR)
01700	(DF VARIT(L)
01800	(PROG(BL)
01900	(COND((ATOM(CAR L))(RETURN(SETQ NO(ADD1 NO))))((EQUAL(CADAR L) @(%))(RETURN(CAAR L))))
02000	(COND((CDAR L)(VARIT1(CDAR L))))
02100	(RETURN (CAR L)) ))
02200	
02300	
02400	(DEFPROP OCTM 
02500	 (LAMBDA(X Y)
02600	  (PROG (Z)
02700	(COND((ATOM X)NIL)((AND(ATOM(CAR X))(NULL(CDR X)))(RETURN(OCFNL(CAR X)Y))))
02800	(SETQ Y(CDR Y))
02850	(SETQ X(LIST X))
02900	   B    (SETQ Z (TERMS1 (LIST (COND ((NEG (CAR Y)) (CDAR Y)) (T (CAR Y)))) 64))
03000	   A    (COND ((UNI X (CAR Z) NIL) (RETURN T)))
03100		(SETQ Z (CDR Z))
03200		(COND (Z (GO A)))
03300		(SETQ Y (CDR Y))
03400		(COND (Y (GO B)))
03500		(RETURN NIL))) 
03600	EXPR)
03700	
03800	(DEFPROP OCFNL 
03900	 (LAMBDA(X Y)
04000	  (PROG NIL
04100		(SETQ Y (CDR Y))
04200	   A    (COND ((COND ((NEG (CAR Y)) (OCR X (CDDAR Y))) (T (OCR X (CDAR Y)))) (RETURN T)))
04300		(SETQ Y (CDR Y))
04400		(COND (Y (GO A)))
04500		(RETURN NIL))) 
04600	EXPR)
04700	
04800	
04900	(DEFPROP OCR 
05000	 (LAMBDA(X Y)
05100	  (COND ((NULL Y) NIL)
05200		((VAR (CAR Y)) (OCR X (CDR Y)))
05300		((CONST (CAR Y)) (COND ((EQ (CAAR Y) X) T) (T (OCR X (CDR Y)))))
05400		((EQ X (CAAR Y)) T)
05500		((OCR X (CDAR Y)) T)
05600		(T (OCR X (CDR Y))))) 
05700	EXPR)